%  {\em Higher-order process calculi} are calculi 
% in which  processes  can be communicated. 
% They 
% have been put forward in the 
% early 1990s,
% with 
%  CHOCS \cite{Tho89}, Plain CHOCS
% \cite{Tho93}, the  Higher-Order $\pi$-calculus 
% \cite{San923}, and others. 
% Higher-order (or process-passing) concurrency is often presented as an
% alternative paradigm 
% to the  first order (or name-passing) concurrency of the $\pi$-calculus
% for the   description of   mobile systems.    
% These calculi are inspired by, and formally close to, the
% $\lambda$-calculus, whose basic computational step --- $\beta$-reduction ---
% involves term instantiation. As in the $\lambda$-calculus, a computational step in higher-order calculi results in the
% instantiation of a variable with a term, which is then
% copied as many times as there are occurrences of the variable. 
%  
% \hocore is a core calculus for higher-order concurrency, 
% recently introduced in \cite{LanesePSS08}.
% It is \emph{minimal}, in that only the operators strictly necessary to obtain
%  higher-order communications are retained. This way, continuations following output messages have been left out, so communication in \hocore is asynchronous.
% %'This way, \hocore is an asynchronous calculus, so continuations 
% %,....For instance,continuations  
% %following  output messages  have been left out.  
% More importantly, \hocore has no restriction
%    operator.
%    Thus all channels are global, and
%     dynamic creation of new channels is impossible.
%     This makes
%     the absence of recursion also relevant, as 
% known encodings of fixed-point combinators in 
% higher-order  process calculi
% require the restriction
% operator.
% The grammar of \hocore processes is:
% \vspace{-1mm}
% \[P :: = \inp a x. P \midd \Ho{a}{P} \midd P \parallel P \midd x \midd \nil \qquad \quad (*)\vspace{-1mm}\]  
% An  input prefixed process 
% $\inp a x . P$ can receive  on
% name (or channel) $a$ a process to be substituted in the place of $x$ in the body $P$;
% an output message  $\Ho{a}{P}$ can send $P$ (the output object) on $a$;  parallel composition 
% allows processes to interact. 
% % \hocore can be seen 
% % as  a kind of concurrent
% % $\lambda$-calculus, where $\inp a x. P$ is a function, with formal
% % parameter $x$ and body $P$, located at  $a$; and
% % $\Ho{a}{P}$ is the argument  for such a function.% located at $a$. 
% %

In higher-order communication there are only two capabilities for received processes: execution and forwarding.
In this chapter we aim at identifying the intrinsic souce of expressive power in \hocore
by studying a limited form of forwarding.
Such a form is obtained from the following syntactic restriction:
output actions can only communicate the parallel composition of known closed processes and processes received through previously executed input actions. 
We study the expressiveness of \hof, the fragment of \hocore featuring this style of communication,
using decidability of termination and convergence of processes as a yardstick. 
Our main result shows that in \hof termination is decidable while convergence is undecidable. 
Then, as a way of recovering the expressiveness loss due to limited forwarding, we extend the calculus
with a form of process suspension called \emph{passivation}. 
The resulting calculus is called \hopf. 
Somewhat surprisingly, in \hopf both termination and convergence are undecidable.
This reveals a great deal of expressive power inherent to forms of suspension such as passivation.

The chapter is structured as follows.
The syntax and semantics of \hof are introduced in Section \ref{s:lang}.
The encoding of Minsky machines into \hof, and the undecidability of convergence are discussed in
Section \ref{s:turing}. The decidability of termination for \hof is addressed in Section \ref{s:wsts}.
The %extension of \hof with passivation, and the associated 
expressiveness results for \hopf are presented in Section \ref{s:passiv}.
Some final remarks, as well as a review of related work, are included in Section \ref{s:hof-conc}.

While the decidability results for \hof have been previously presented as
\citep{GiustoPZ09}, the extension of \hof with passivation and its associated decidability results
are original to this dissertation.

\section{Introduction}
Despite its minimality, 
%via a termination preserving 
in Chapter \ref{chap:core}
\hocore was shown to be Turing complete by exhibiting an
encoding of Minsky machines.\footnote{
Along the paper
we use the appellations ``Turing complete'' and ``weak Turing complete'' as in the 
criteria defined by \cite{Bravetti09} and discussed in Section \ref{ss:expr-approaches}.}
Therefore, properties such as 
\begin{itemize}
 \item \emph{termination}, i.e., non existence of divergent computations
\item \emph{convergence}, i.e., existence of a terminating computation
\end{itemize}
are both undecidable in \hocore\footnote{Termination and convergence are sometimes also referred to as \emph{universal} and \emph{existential} termination, respectively.}. 
In contrast, somewhat surprisingly, strong bisimilarity is decidable, and 
%Furthermore, 
several sensible bisimilarities %in the higher-order setting
 coincide with it. 


In this chapter, 
we shall aim at identifying the intrinsic source of expressive power in \hocore.
%It can be said that a 
%Our initial observation is that a
A
 substantial part of the expressive power of a concurrent language comes from the ability of accounting for infinite behavior. In higher-order process calculi there is no explicit operator for such a behavior, as both recursion and replication can be encoded. We then find that infinite behavior % is devoted to this aim, this feature 
resides in 
the interplay of higher-order communication, in particular, in 
the ability of %receiving a process and 
\emph{forwarding} 
a received process within
an \emph{arbitrary context}. % containing a received process.
%More precisely, 
For instance, 
consider the process $R = a(x).\Ho{b}{P_x}$,
where $P_x$ stands for a process $P$ with free occurrences of a variable $x$.  
Intuitively, $R$ receives a process on name $a$ and forwards it on name $b$. 
It is easy to see that since 
%objects in output actions are built following the syntax given by $(*)$, 
there are no limitations on the structure of objects in output actions, 
the actual structure of 
$P_x$ can be fairly complex. 
One could even ``wrap'' the process to be received in $x$ using an arbitrary number of $k$ ``output layers'', i.e., by letting
$P_x = \Ho{b_1}{\Ho{b_2}{\ldots \Ho{b_k}{x}}\ldots}$. 
This \emph{nesting capability} embodies a great deal of the expressiveness of \hocore: as a matter of fact, 
the encoding of Minsky machines in %\cite{LanesePSS08} 
\hocore
depends critically on nesting-based counters.
Therefore, investigating suitable limitations to the 
kind of processes that can be communicated in an output action appears as a legitimate approach to assess the expressive power of higher-order concurrency.

With the above consideration in mind, 
in this chapter 
we propose \hof, a sublanguage of \hocore in which output actions 
are limited so as to rule out the nesting capability (Section \ref{s:lang}). In \hof, 
output actions can communicate
the parallel composition of
two kinds of objects: 

\begin{enumerate}
 \item closed processes (i.e., processes that do not contain free variables), and 
\item processes received through previously executed input actions.
\end{enumerate}

Hence, the context in which the output action resides can only contribute to communication by
``appending'' pieces of code that admit no inspection, available in the form of a black-box.
More precisely, the grammar of \hof processes is 
the same as that 
of \hocore, 
%in $(*)$, 
except for the production for output actions, which is replaced by the following one:
\[
\Ho{a}{ x_1 \parallel \cdots \parallel x_k \parallel P} \vspace{-2mm}
\]
where $k \geq 0$ and $P$ is a closed process.
This modification directly restricts forwarding capabilities for output processes, which in turn, leads to a more limited structure of processes along reductions.

%In addition to the above motivations, %related to expressiveness, 
The limited style of higher-order communication enforced in \hof 
%turns out to be interesting 
is relevant from a pragmatic perspective.
In fact, communication in \hof 
is inspired by those cases in which a process $P$
is communicated in a translated format $\encp{P}{}$,
and the translation is not compositional. That is, the cases in which, 
for any  process context $C$, 
the translation of $\ct{P}$ cannot be seen as a function of
the translation of $P$, i.e.,
%$\encp{ \ct{P}}{} \neq \encp{ C}{}[\encp{P}{}]$.
there exists no context $D$ such that
$\encp{ \ct{P}}{} = D[P]$.

More concretely, communication as in \hof
%This setting 
can be related to several existing programming scenarios. 
The simplest example is perhaps mobility of already compiled code, 
on which it is not possible to
apply inverse translations (such as
reverse engineering).
Other examples include \emph{proof-carrying code} \citep{NeculaL98}
and communication of \emph{obfuscated code} \citep{CollbergTL98}. %\cite{CollbergT02}.
The former features communication of executable code that comes with a certificate: 
a recipient can only check the certificate and decide whether to execute the code or not.
The latter consists of the communication of 
source code that is made difficult to understand for, e.g., security/copyright reasons, while preserving its functionality.

% Furthermore, forms of forwarding are also common to \emph{adapters}, i.e.
% software artifacts used as part of evolvability patterns of software libraries (services, components) 
% to guarantee backward compatibility.
% In that context, when a library (service, component) 
% needs to be updated with a new version,
% an adaptor is used: it works like as a ``proxy'' that receives
% requests from clients/users (that only know the interface of the old library)
% and forwards them a modified request that respects the interface of the new version of the library (service, component).
% This evolvability pattern is the one implemented in versions of Linux that feature new
% versions of libraries for system devices.
% An adapter written in \hof would have the capability of 
% enriching such requests by, for instance, appending pieces of code to them.

In this chapter
%The main contribution of the chapter is the 
we 
study the expressiveness of \hof 
using 
%in terms of 
decidability of termination and convergence of processes as a yardstick. 
Our main results are:
\begin{description}
 \item[Undecidability of Convergence in \hof.] 
Similarly as in \hocore, in \hof 
it is possible to encode Minsky machines.
%is shown to be Turing complete %(Section \ref{s:turing})
%by exhibiting an encoding of Minsky machines into \hof.
The calculus thus retains a significant expressive power despite of the limited forwarding capability.
Unlike 
%the encoding of Minsky machines in 
\hocore, however, 
\hof is only weakly Turing complete.
In fact, the encoding of Minsky machines in \hof 
is \emph{not faithful}
for it may introduce computations which do not correspond to the expected
behavior of the modeled machine. 
Such computations %introduced by the encoding
are forced to be infinite and
thus regarded as non-halting computations which are therefore ignored. 
%Only the finite computations correspond to those of the encoded Minsky machine.
This allows us to prove that a Minsky machine terminates if and only if its encoding in \hof converges. 
Consequently, convergence in \hof is \emph{undecidable}.

\item[Decidability of Termination in \hof.] 
In sharp contrast with \hocore, termination in \hof is \emph{decidable}. % (Section \ref{s:wsts}).
This result is obtained by appealing to the theory of \emph{well-structured transition systems} 
\citep{Finkel90,AbdullaCJT00,FinkelS01}, following the approach used by \cite{Busi09}.
%As for (2), %although relying on 
% While the use of well-structured transition systems is certainly not a new approach to obtain 
% decidability 
% %expressiveness 
% results,
% %However, 
To the best of our knowledge, this is the first time 
the theory of well-structured transition systems
is applied in a higher-order concurrency setting. 
This is significant because
the adaptation to the \hof case is far from trivial. Indeed, as we shall discuss, 
this approach %based on WSTS 
relies on %over-
defining
%approximating %a bound on the (set of) derivatives of a process.
%CORREGGERE 
an upper bound on the \emph{depth} of the
(set of) derivatives of a process.
By depth of a process we mean its
maximal nesting of input/output actions.
Notice that, even with the limitation on forwarding enforced by \hof, because of the ``term copying'' feature of higher-order calculi, 
variable instantiation %of a variable with a process
might lead to a potentially larger process. 
Hence, finding suitable ways of bounding 
the set of derivatives of a process is rather challenging and needs care. 

\item[Undecidability of Termination \emph{and} Convergence in \hof with Passivation.]
The decidability of termination in \hof provides compelling evidence 
on the fact that the limited forwarding %communication 
entails a loss of expressive power for \hocore.
It is therefore legitimate 
to investigate whether such an expressive power can be recovered
while preserving the essence of the limited 
forwarding
%output actions as 
in \hof.
For this purpose, we extend \hof with a \emph{passivation} construct that
allows to \emph{suspend} the execution of a running process.
Forms of process suspension (such as passivation)
are of both practical and theoretical interest 
%as the formalized by passivation operators are relevant nowadays, 
as they are at the heart of mechanisms for \emph{dynamic system reconfiguration}.
The extension of \hof with passivation, called \hopf, is shown to be Turing complete
by exhibiting a \emph{faithful} encoding of Minsky machines.
Therefore, in \hopf \emph{both} convergence and termination are \emph{undecidable}. % in the extended \hof.
To the best of our knowledge, 
ours is the first result on the expressiveness and decidability of 
constructs for process suspension in the context of 
higher-order process calculi.
\end{description}






%\shortv{\noindent {\bf Structure of the paper.}}
%\longv{\paragraph{\bf Structure of the paper.} 

%Due to a lack of space, we omit most proofs; they are included in the extended version of this paper

